the_w:World, l:IdLnk, t:. m(l;t)  Msg List 

latex

Definitions	World, Msg, m(l;t), w.M, m(i;t), onlnk(l;mss), filter(P;l), a = b, S  T, Msg(M), Id, source(l), mlnk(m), x:A. B(x), , t  T, IdLnk
Lemmas	IdLnk wf, nat wf, mlnk wf, lsrc wf, Id wf, eq lnk wf, Msg wf, filter wf, world wf